Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:	eq(0,0)	→ true
2:	eq(0,s(Y))	→ false
3:	eq(s(X),0)	→ false
4:	eq(s(X),s(Y))	→ eq(X,Y)
5:	le(0,Y)	→ true
6:	le(s(X),0)	→ false
7:	le(s(X),s(Y))	→ le(X,Y)
8:	min(cons(0,nil))	→ 0
9:	min(cons(s(N),nil))	→ s(N)
10:	min(cons(N,cons(M,L)))	→ ifmin(le(N,M),cons(N,cons(M,L)))
11:	ifmin(true,cons(N,cons(M,L)))	→ min(cons(N,L))
12:	ifmin(false,cons(N,cons(M,L)))	→ min(cons(M,L))
13:	replace(N,M,nil)	→ nil
14:	replace(N,M,cons(K,L))	→ ifrepl(eq(N,K),N,M,cons(K,L))
15:	ifrepl(true,N,M,cons(K,L))	→ cons(M,L)
16:	ifrepl(false,N,M,cons(K,L))	→ cons(K,replace(N,M,L))
17:	selsort(nil)	→ nil
18:	selsort(cons(N,L))	→ ifselsort(eq(N,min(cons(N,L))),cons(N,L))
19:	ifselsort(true,cons(N,L))	→ cons(N,selsort(L))
20:	ifselsort(false,cons(N,L))	→ cons(min(cons(N,L)),selsort(replace(min(cons(N,L)),N,L)))

There are 16 dependency pairs:


21:	EQ(s(X),s(Y))	→ EQ(X,Y)
22:	LE(s(X),s(Y))	→ LE(X,Y)
23:	MIN(cons(N,cons(M,L)))	→ IFMIN(le(N,M),cons(N,cons(M,L)))
24:	MIN(cons(N,cons(M,L)))	→ LE(N,M)
25:	IFMIN(true,cons(N,cons(M,L)))	→ MIN(cons(N,L))
26:	IFMIN(false,cons(N,cons(M,L)))	→ MIN(cons(M,L))
27:	REPLACE(N,M,cons(K,L))	→ IFREPL(eq(N,K),N,M,cons(K,L))
28:	REPLACE(N,M,cons(K,L))	→ EQ(N,K)
29:	IFREPL(false,N,M,cons(K,L))	→ REPLACE(N,M,L)
30:	SELSORT(cons(N,L))	→ IFSELSORT(eq(N,min(cons(N,L))),cons(N,L))
31:	SELSORT(cons(N,L))	→ EQ(N,min(cons(N,L)))
32:	SELSORT(cons(N,L))	→ MIN(cons(N,L))
33:	IFSELSORT(true,cons(N,L))	→ SELSORT(L)
34:	IFSELSORT(false,cons(N,L))	→ SELSORT(replace(min(cons(N,L)),N,L))
35:	IFSELSORT(false,cons(N,L))	→ REPLACE(min(cons(N,L)),N,L)
36:	IFSELSORT(false,cons(N,L))	→ MIN(cons(N,L))

The approximated dependency graph contains 5 SCCs: {21}, {22}, {23,25,26}, {27,29} and {30,33,34}.

Consider the SCC {21}. There are no usable rules. By taking the AF π with π(EQ) = 1 together with the lexicographic path order with empty precedence, rule 21 is strictly decreasing.

Consider the SCC {22}. There are no usable rules. By taking the AF π with π(LE) = 1 together with the lexicographic path order with empty precedence, rule 22 is strictly decreasing.

Consider the SCC {23,25,26}. The usable rules are {5-7}. By taking the AF π with π(MIN) = 1, π(IFMIN) = 2, π(le) = [ ] and π(cons) = [2] together with the lexicographic path order with precedence le ≻ false and le ≻ true, the rules in {7,23} are weakly decreasing and the rules in {5,6,25,26} are strictly decreasing.

Consider the SCC {27,29}. The usable rules are {1-4}. By taking the AF π with π(REPLACE) = 3, π(IFREPL) = 4, π(eq) = [ ] and π(cons) = [2] together with the lexicographic path order with precedence eq ≻ false and eq ≻ true, the rules in {4,27} are weakly decreasing and the rules in {1-3,29} are strictly decreasing.

Consider the SCC {30,33,34}. The usable rules are {1-16}. By taking the AF π with π(min) = π(SELSORT) = 1, π(ifmin) = π(IFSELSORT) = 2, π(replace) = 3, π(ifrepl) = 4, π(eq) = π(le) = π(s) = [ ] and π(cons) = [2] together with the lexicographic path order with precedence eq ≻ false, eq ≻ true, le ≻ false, le ≻ true, nil ≻ 0 and nil ≻ s, the rules in {4,7,10,13-16,30} are weakly decreasing and the rules in {1-3,5,6,8,9,11,12,33,34} are strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (1.78 seconds) --- May 3, 2006